home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
BMUG Revelations
/
BMUG Revelations.toast
/
Programming
/
Programming Languages
/
XLisp 2.1e3
/
lisp
/
qa.lsp
< prev
next >
Wrap
Text File
|
1992-10-29
|
37KB
|
1,243 lines
;========================================================================
;
; qa.lsp - Question answering program using set-of-support
; unit-preference resolution principles.
;
; Author: John W. Ward (jwward)
; Date: 06-Dec-86
;
; The following program was written for an Artificial Intelligence
; class at Kent State University. The testing sequence used was designed
; specifically to fit class requirements. The program is offered for
; inspection and experimentation. The only claim I make regarding the
; program is that I enjoyed working on it and learned something from it.
;
; Some of the algorithms and examples follow our textbook: Artificial
; Intelligence, by Elaine Rich (McGraw-Hill, 1983).
;
;-------------------------------------------------------------------------
;
; Known limitations: The program degrades quickly when there is
; a relatively high branching factor (i.e. many possible paths). When
; the pairs variable gets too big, something nasty usually happens. On
; my machine the something nasty is a warm restart.
;
; The program was written in XLISP 1.7. Converted to XLISP 2.0
; by David Betz.
;
;-------------------------------------------------------------------------
; QA.LOG provides a transcript of a program session.
;-------------------------------------------------------------------------
;
; Question-answering is done as follows:
; 1) The question is negated, then converted to clause form with the
; original question tacked on in a $SUCCESS$ "literal".
; 2) Each clause of the question is paired with all members of base,
; producing the original "pairs" list. Insertion to the list are
; according to size of smaller clause * 1000 + size of larger clause.
; Each clause is then added to the "base", which thus contains the
; set-of-support as well.
; 3) Until solution is found (and user specifies QUIT) or "pairs" is
; exhausted or the number of pairs tested exceeds a set limit (400):
; a) Take the next pair of clauses from "pairs". Try to resolve by
; attempting to unify any pair of literals having opposite sign.
; b) If the unification is successful, produce the resolution.
; If resolution produces a clause already in the base, ignore it.
; Otherwise, if the resolution is a success state, display and
; ask the user for MORE or QUIT.
; Otherwise (new, non-success result), add the result paired with
; all current members of the base cum set-of-support to "pairs",
; then add the result to the base.
;
; Practically, this thing is slow and perverse. It's amazing how long
; it takes to exhaust the possibilities of an obviously wrong path.
;
; Data structures and variables:
; base - List of hypotheses and set-of-support. The
; set-of-support can be distinguished by a $success$
; clause. Each clause is actually a list, with the
; clause proceeded by its literal-count.
; pairs - List of clause-pairs to consider for resolution.
; Entries are triples - combined literal-count,
; left-clause and right-clause. Sorted on ascending
; literal-count, with new entries following old ones
; to provide results analogous to a breadth-first
; search. (New preceding old ends up close to depth-
; first.)
; q-clause - S-o-s clause currently under consideration (LHS)
; b-clause - Base clause currently under consideration (RHS)
; subst-list - Composition of all substitutions used in
; resolution. This can be applied to the
; query to produce a solution. (I hope!)
; names - Names in use in the base including variable names,
; predicates, and Skolem functions. The type of
; each name will be attached to it.
; (I will convert variables on initial entry into
; the base or query, thus avoiding renaming later.
; I hope!)
;
; Naming:
; Constants - begin with letters A through F or with $.
; (XLISP converts input to upper-case, so I can't
; distinguish that way.)
; Variables - Begin with G through Z.
;
; Associate with every element of a clause is its type - CONSTANT or
; VARIABLE.
;
;=========================================================================
;
(alloc 1000)
(expand 20)
;
;-------------------------------------------------------------------
;
; qa - main routine
;
; The program is in assert or question mode. In question mode,
; it will attempt to answer the question given by the user. In
; assert mode, it will add to the fact base.
;
; Special commands:
; assert - Change to assert mode
; question - Change to question mode
; end - Start with a new base of information
; nil - End the program
;
;-------------------------------------------------------------------
(defun qa ()
; First time
(init-qa)
; Main loop for each base set
(do
() ; No initialization
((or (null in-line) (equal in-line 'end)))
(setq in-line (get-input mode))
(cond
((null in-line) nil)
((equal in-line 'end) (init-qa))
((equal in-line 'assert) (setq mode in-line))
((equal in-line 'question) (setq mode in-line))
((equal in-line 'base)
(mapcar `(lambda (a) (print (cadr a))) base)
)
((equal in-line 'proof)
(setq show-proof (not show-proof))
(cond
(show-proof (princ "Resolutions will be shown.\n"))
(t (princ "Only answers will be shown.\n"))
)
)
((equal in-line 'unify)
(setq show-unify (not show-unify))
(cond
(show-unify (princ "Unifications will be shown.\n"))
(t (princ "Unifications will not be shown.\n"))
)
)
((equal in-line 'pairs)
(setq show-pairs (not show-pairs))
(cond
(show-pairs (princ "Clause-pairs will be shown.\n"))
(t (princ "Clause-pairs will be shown.\n"))
)
)
((equal in-line 'help) (give-help))
((equal mode 'question) (answer in-line))
(t (assume in-line))
)
)
)
;
;-------------------------------------------------------------------
;
; Provide simple help messages
;
(defun give-help ()
(princ "\n\n\tQA - Help\n\n")
(princ "Commands:\n")
(princ "\tNil to exit, End to restart\n")
(princ "\tProof, Unify, and Pairs toggle display settings\n")
(princ "\tAssert - Shift to assertion mode\n")
(princ "\tQuestion - Shift to question mode\n")
(princ "\tBase - Display base assumptions\n")
(princ "\tHelp - Print this message\n")
(princ "\nInput form:\n\n")
(princ "\tConstants begin with letters A-E or $.\n\n")
(princ "\tEnter assertions or questions in LISP-like form. You may\n")
(princ "include the operators AND, OR, NOT, IMPLY, AND EQUIV. Thus,\n")
(princ "to indicate that a male parent is a father, type:\n\n")
(princ "\t(EQUIV (AND ($PARENT X Y) ($MALE X)) ($FATHER X Y))\n\n")
(princ "The definition of commutative binary operations is:\n\n")
(princ "\t(IMPLY ($COMMUT K) (EQUIV (K X Y Z) (K Y X Z)))\n")
)
;-------------------------------------------------------------------
;
; Attempt to answer the question
;
(defun answer (question)
(let
(
(c-question nil)
)
(setq pairs nil)
(setq
c-question
(clause-convert `(or (not ,question) ($success$ ,question)))
)
(cond
((equal (car c-question) 'and)
(setq c-question (mapcar 'set-types c-question))
(mapcar 'add-sos (cdr c-question))
)
(t
(setq c-question (set-types c-question))
(add-sos c-question)
)
)
(solve)
(princ "\n\nDone.\n\n")
(setq base (remove-success base))
)
)
;
;-------------------------------------------------------------------
;
; Find solution to the question -
;
;
; pairs = (question X base) from set-up
; done <-- nil
; While pairs != nil and done == nil {
; pair <-- (car pairs); pairs <-- (cdr pairs);
; Get q-clause and b-clause from pair
; <<< solve-clause-clause >>>
; For each q-literal in q-clause {
; <<< solve-lit-clause >>>
; For each b-literal of opposite sign in b-clause {
; <<< solve-lit-lit >>>
; subs <-- unification of q-literal and b-literal
; If subs != nil {
; Make subs in q-clause and b-clause
; resolution <-- resolve of q-clause and b-clause
; <<< resolved >>>
; Report resolution
; If resolution is a success-state {
; return true if they don't want More
; }
; else {
; add (resolution X base) to pairs
; add resolution to base
; return nil (keep going)
; }
; }
; }
; }
; }
;
;
(defun solve ()
(setq solutions-found nil)
(setq pairs-count 0)
(do
(
(done nil)
(pair nil)
)
(
(or done (null pairs) (>= pairs-count max-pairs))
)
(setq pair (car pairs))
(setq pairs (cdr pairs))
(setq q-clause (cadr pair))
(setq b-clause (caddr pair))
(setq done (solve-clause-clause))
)
)
;-------------------------------------------------------------------
;
; Test if result is a success
;
;
(defun success-p (clause)
(cond
((atom clause) nil)
((equal (car (first-lit clause)) '$success$) t)
(t nil)
)
)
;-------------------------------------------------------------------
;
; Solve given two clauses - pass on with full clauses for later
; breakup
;
; <<< solve-clause-clause >>>
; Add b-clause to right-used
; For each q-literal in q-clause {
; <<< solve-lit-clause >>>
; }
;
(defun solve-clause-clause ()
(cond
(show-pairs
(princ "Working on clauses:\n")
(print q-clause)
(print b-clause)
(terpri)
)
)
(setq pairs-count (1+ pairs-count))
(cond
((equal (rem pairs-count 50) 0)
(princ "Pairs count:\t") (print pairs-count)
(princ "Base:\t\t") (print (length base))
(princ "Pairs:\t\t") (print (length pairs))
(princ "Size:\t\t") (print (deep-count pairs))
(terpri)
(gc)
(mem)
(terpri)
)
)
(solve-clause-clause* (remove-success q-clause) (remove-success b-clause))
)
(defun solve-clause-clause* (q-work b-work)
(let
(
(result nil)
)
(cond
((null b-work) nil)
((atom b-work)
(princ "Error in solve-clause-clause* - b-work is atom\n")
nil
)
((null q-work) nil)
((atom q-work)
(princ "Error in solve-clause-clause* - q-work is atom\n")
nil
)
(
(setq result (solve-lit-clause (first-lit q-work) b-work))
result
)
(t (solve-clause-clause* (remove-first-lit q-work) b-work))
)
)
)
;-------------------------------------------------------------------
;
; Solve with a question literal and a base clause
;
; <<< solve-lit-clause >>>
; For each b-literal of opposite sign in b-clause {
; <<< solve-lit-lit >>>
; }
;
;
(defun solve-lit-clause (q-lit b-work)
(let
(
(result nil)
)
(cond
((null q-lit) nil)
((atom q-lit)
(princ "Error in solve-lit-clause - q-lit is atom\n")
nil
)
((null b-work) nil)
((atom b-work)
(princ "Error in solve-lit-clause - b-work is atom\n")
nil
)
((setq result (solve-lit-lit q-lit (first-lit b-work))) result)
(t (solve-lit-clause q-lit (remove-first-lit b-work)))
)
)
)
;-------------------------------------------------------------------
;
; Solve with a question literal and a base literal
;
; <<< solve-lit-lit >>>
; subs <-- unification of q-literal and b-literal
; If subs != nil {
; Make subs in q-clause and b-clause
; resolution <-- resolve of q-clause and b-clause
; If resolution != nil {
; <<< resolved >>>
; }
; }
;
;
(defun solve-lit-lit (q-lit b-lit)
(let
(
(subs nil)
(resolution nil)
(old-q q-clause)
(old-b b-clause)
)
; Quit without effort if literals are not of opposite sign
(cond
((equal (lit-sign q-lit) (lit-sign b-lit)) nil)
(t
(setq subs (unify q-lit b-lit))
(cond
(show-unify
(princ "Unification of: ") (print q-lit)
(princ " and: ") (print b-lit)
(princ " is: ") (print subs)
(terpri)
)
)
(cond
((not (null subs))
(setq old-q (make-subs subs q-clause))
(setq old-b (make-subs subs b-clause))
(setq resolution (resolve old-q old-b))
(cond
(
(not
(member
(add-count resolution)
base :test #'equal
)
)
(resolved resolution)
)
(t nil)
)
)
(t nil)
)
)
)
)
)
;-------------------------------------------------------------------
;
; Handle a successful resolution
;
; Report resolution
; If resolution is a success-state {
; done <-- quit if they don't want More
; }
; else {
; add (resolution X base) to pairs
; add resolution to base
; return nil for resolution
; }
;
(defun resolved (resolution)
(cond
(show-proof
(terpri)
(princ "Clause 1 ") (print q-clause)
(princ "Clause 2 ") (print b-clause)
(princ "Resolution ") (print resolution)
(terpri)
)
)
(cond
((success-p resolution)
(cond
(
(not
(member
resolution
solutions-found :test #'equal
)
)
(setq
solutions-found
(append solutions-found (list resolution))
)
(print (first-lit resolution))
(terpri)
(princ "Enter QUIT to quit, MORE for more solutions --")
(equal (read) 'quit)
)
(t nil)
)
)
(t
(add-sos resolution)
nil
)
)
)
;-------------------------------------------------------------------
;
; Determine sign of literal (either NOT or NIL)
;
;
(defun lit-sign (lit)
(cond
((atom lit) nil)
((equal (car lit) 'not) 'not)
(t nil)
)
)
;-------------------------------------------------------------------
;
; Return the "absolute value" (NOT removed) of lit
;
;
(defun lit-abs (lit)
(cond
((null (lit-sign lit)) lit)
(t (cadr lit))
)
)
;-------------------------------------------------------------------
;
; Return the negation of a literal
;
;
(defun lit-negative (lit)
(cond
((null (lit-sign lit)) `(not ,lit))
(t (cadr lit))
)
)
;-------------------------------------------------------------------
;
; Unify two literals - (from the book, page 156)
;
;
(defun unify (q-lit b-lit)
(unify* (lit-abs q-lit) (lit-abs b-lit) nil)
)
(defun unify* (q-lit b-lit subs)
(cond
; If either is an atom, they must be equal or
; at least one a variable, else fail
((or (atom q-lit) (atom b-lit))
(cond
((equal q-lit b-lit) (compose subs '(nil nil)))
((variable-p b-lit) (compose subs (ok-sub b-lit q-lit)))
((variable-p q-lit) (compose subs (ok-sub q-lit b-lit)))
(t nil)
)
)
; We get here for lists
((/= (length q-lit) (length b-lit)) nil)
(t
(setq subs (unify* (car q-lit) (car b-lit) subs))
(cond
((null subs) nil)
(t
(unify*
(make-subs subs (cdr q-lit))
(make-subs subs (cdr b-lit))
subs
)
)
)
)
)
)
;-------------------------------------------------------------------
;
; Return nil if y contains x, else return (x y)
;
;
(defun ok-sub (x y)
(cond
((deep-member x y) nil)
(t `(,x ,y))
)
)
;-------------------------------------------------------------------
;
; Compose single substitution y into list x
;
;
(defun compose (x y)
(let
(
(result nil)
)
(cond
((null y) nil)
((null x) (list y))
((equal x '((nil nil))) (list y))
(t
(setq x (sub-right-side y x))
(cond
((assoc (car y) x) x)
(t (append x (list y)))
)
)
)
)
)
;-------------------------------------------------------------------
;
; Make all substitutions sub (a b) into substitution list
; of the form ((x a)) --> ((x b))
;
;
(defun sub-right-side (sub sub-list)
(mapcar `(lambda (x) (sub-right-side* ',sub x)) sub-list)
)
(defun sub-right-side* (sub sub-entry)
(cons
(car sub-entry)
(make-subs (list sub) (cdr sub-entry))
)
)
;-------------------------------------------------------------------
;
; Is x variable?
;
;
(defun variable-p (x)
(cond
((null x) nil)
((atom x) (equal (get x 'type) 'variable))
(t nil)
)
)
;-------------------------------------------------------------------
;
; Resolve two unified clauses
;
;
(defun resolve (clause-1 clause-2)
(let
(
(result nil)
)
(setq success-list '(or))
(setq clause-1 (strip-success clause-1))
(setq clause-2 (strip-success clause-2))
(setq result (load-lits (lit-factor clause-1) '(or)))
(setq result (load-lits (lit-factor clause-2) result))
(setq result (load-lits success-list result))
result
)
)
;-------------------------------------------------------------------
;
; Return clause less all $success$ literals and record $success$
; literals in success-list
;
;
(defun strip-success (clause)
(cond
((null clause) nil)
((atom clause) nil) ; Should be an error
((equal (car clause) '$success$)
(setq success-list (load-lits clause success-list))
nil
)
((literal-p clause) clause)
(t ; Begins with OR
(remove
nil
(cons (car clause) (mapcar 'strip-success (cdr clause)))
)
)
)
)
;-------------------------------------------------------------------
;
; Before we turn the clauses loose on each other, factor any
; internally repeated literals. If there are internal opposite
; literals, return nil, thus letting the other clauses be unaffected
; by the tautology.
;
;
(defun lit-factor (clause)
(lit-factor* clause '(or))
)
(defun lit-factor* (clause new-clause)
(let
(
(first (first-lit clause))
(rest (remove-first-lit clause))
)
(cond
((null clause) new-clause)
((member first new-clause :test #'equal)
(lit-factor* rest new-clause)
)
((member (lit-negative first) new-clause :test #'equal) nil)
(t (lit-factor* rest (append new-clause (list first))))
)
)
)
;-------------------------------------------------------------------
;
; Add literals to clause -
; If literal's negative is in clause, remove from both clauses
; If literal is in clause, don't add it.
; Otherwise add at end of clause
;
;
(defun load-lits (clause new-clause)
(let
(
(first (first-lit clause))
(rest (remove-first-lit clause))
(negative nil)
)
(setq negative (lit-negative first))
(cond
((null clause) new-clause)
((member first new-clause :test #'equal)
(load-lits rest new-clause)
)
((member negative new-clause :test #'equal)
(load-lits rest (remove negative new-clause :test #'equal))
)
(t (load-lits rest (append new-clause (list first))))
)
)
)
;-------------------------------------------------------------------
;
; Make substitutions from substitution list
;
(defun make-subs (subs clause)
(let
(
(pair nil)
)
(cond
((null clause) nil)
((atom clause)
(setq pair (assoc clause subs))
(cond
((null pair) clause)
(t (cadr pair))
)
)
(t (mapcar `(lambda (x) (make-subs ',subs x)) clause))
)
)
)
;-------------------------------------------------------------------
;
; Add fact to the base hypotheses
;
; Convert the fact to clause form.
; If the result is a conjuction of clauses, set types and add them all;
; else set the types and add the single clause.
;
(defun assume (fact)
(setq fact (clause-convert fact))
(cond
((equal (car fact) 'and)
(setq fact (mapcar 'set-types fact))
(setq base (append base (mapcar 'add-count (cdr fact))))
)
(t
(setq fact (set-types fact))
(setq base (append base (list (add-count fact))))
)
)
fact
)
;-------------------------------------------------------------------
;
; Return clause in a list preceded by the clause's literal-count
;
(defun add-count (clause)
(list (literal-count clause) clause)
)
;-------------------------------------------------------------------
;
; Add a clause to the set-of-support -
; add (clause X base) to pairs;
; add clause to base
;
(defun add-sos (clause)
(let
(
(pair (list (literal-count clause) clause))
)
(mapcar `(lambda (a) (add-pair pair a)) base)
(setq base (append base (list (add-count clause))))
)
)
;-------------------------------------------------------------------
;
; Insert a pair of clauses into pairs - returns pairs
;
(defun add-pair (q b)
(let
(
(size-q (car q))
(size-b (car b))
(q-cl (cadr q))
(b-cl (cadr b))
(size 0)
(new-pair nil)
)
(cond
((< size-q size-b)
(setq size (+ (* 1000 size-q) size-b))
(setq pairs (insert-pair (list size q-cl b-cl) pairs))
)
(t
(setq size (+ (* 1000 size-b) size-q))
(setq pairs (insert-pair (list size b-cl q-cl) pairs))
)
)
)
)
;-------------------------------------------------------------------
;
; Insert pair into pairs list - return new list
;
(defun insert-pair (pair pair-list)
(cond
((null pair-list) (list pair))
; Use <= for "depth-first", < for "breadth-first"
((< (car pair) (caar pair-list)) (cons pair pair-list))
(t (cons (car pair-list) (insert-pair pair (cdr pair-list))))
)
)
;-------------------------------------------------------------------
;
; Count the literals in a clause
; Ignore a success clause and change 2's to 1 [e.g. (OR (A)) --> (A)]
;
(defun literal-count (clause)
(setq clause (remove-success clause))
(cond
((atom clause) 0)
((literal-p clause) 1)
(t (1- (length clause)))
)
)
;-------------------------------------------------------------------
;
; Return the clause with any $success$ element removed
;
(defun remove-success (clause)
(cond
((atom clause) clause)
(t (remove nil (remove '$success$ clause :test #'deep-member)))
)
)
;-------------------------------------------------------------------
;
; Set the types for each name in the new line
;
; Uses the global association list new-names
;
; If a clause is nil, return nil.
; If it's an atom, type it as variable or constant with separate routine.
; If it's a list, pass the set-types through on mapcar.
;
(defun set-types (clause)
(setq new-names nil)
(set-types* clause)
)
(defun set-types* (clause)
(cond
((null clause) nil)
((equal clause 'not) clause)
((equal clause 'or) clause)
((equal clause 'and) clause)
((atom clause) (set-unit-type clause))
(t (mapcar 'set-types* clause))
)
)
;
;-------------------------------------------------------------------
;
; Set the type for an atom - either constant or variable
;
; For constants:
; Add name to names if new.
;
; For variables:
; Is the name is already in the new-names list?
; Yes : return the associated name.
; No : Is the name in names?
; Yes : Find an alternate name, add the substitution pair to
; new-names, add the new name to names with type variable
; and return the new name.
; No : Add the name to names with type variable, add an identity
; pair to new-names, return the original.
;
(defun set-unit-type (atm)
(let
(
(g-symb atm) ; Substitution name
(atm-type 'variable)
(pair nil)
)
(cond
((equal (get atm 'type) 'constant) nil)
((char> (char (symbol-name atm) 0) #\F)
; If first character > F, it's a variable.
(setq pair (assoc atm new-names))
(cond
((not (null pair)) (setq g-symb (cadr pair)))
(t
(cond
((member atm names)
(setq g-symb (gensym))
(add-new-name atm g-symb)
)
(t (add-new-name atm atm))
)
)
)
)
)
(add-name g-symb)
)
)
;
;-------------------------------------------------------------------
;
; If the atom is not found in names, add it with given type.
; Return the atom
;
(defun add-name (atm)
(cond
((member atm names) atm)
(t (setq names (cons atm names)))
)
(cond
((get atm 'type) nil)
((char<= (char (symbol-name atm) 0) #\F) (putprop atm 'constant 'type))
(t (putprop atm 'variable 'type))
)
atm
)
;
;-------------------------------------------------------------------
;
; Add a new name to the new-names a-list. Return the substitution
; value
;
(defun add-new-name (x y)
(setq new-names (cons (list x y) new-names))
y
)
;-------------------------------------------------------------------
;
; Find x at any depth in list
;
(defun deep-member (x lst)
(cond
((equal x lst) t)
((atom lst) nil)
((deep-member x (car lst)) t)
(t (deep-member* x (cdr lst)))
)
)
(defun deep-member* (x lst) ; To avoid x = cdr
(cond
((null lst) nil)
((deep-member x (car lst)) t)
(t (deep-member* x (cdr lst)))
)
)
;-------------------------------------------------------------------
;
; Print prompt and get input
;
(defun get-input (mode)
(terpri)
(cond
((equal mode 'assert) (princ "Assert --"))
(t (princ "Question --"))
)
(read)
)
;
;-------------------------------------------------------------------
;
; Test if x is a literal
;
(defun literal-p (x)
(cond
((atom x) nil)
((equal (car x) 'not)
(not (member (caadr x) (cons 'not operators)))
)
((member (car x) operators) nil)
(t t)
)
)
;-------------------------------------------------------------------
;
; Find first literal in x
;
(defun first-lit (x)
(cond
((atom x) nil)
((equal (car x) 'or) (cadr x))
(t x)
)
)
;-------------------------------------------------------------------
;
; Return x with first literal removed (keep OR unless down to one literal
;
(defun remove-first-lit (x)
(cond
((atom x) nil)
((literal-p x) nil) ; If not, must be clause
((equal (car x) '$success$) nil)
((<= (length x) 3) (car (cdr (cdr x))))
(t (cons 'or (cdr (cdr x))))
)
)
;-------------------------------------------------------------------
;
; Count the items in a list - for memory test purposes
;
(defun deep-count (x)
(cond
((null x) 0)
((atom x) 1)
(t
(apply '+ (mapcar 'deep-count x))
)
)
)
;-------------------------------------------------------------------
;
; Set global variables to initial states
;
(defun init-qa ()
(setq base nil)
(setq names '(not or))
(setq show-proof t)
(setq show-unify nil)
(setq show-pairs nil)
(setq max-pairs 400)
(putprop 'not 'constant 'type)
(putprop 'or 'constant 'type)
(putprop '$success$ 'constant 'type)
(putprop 'and 'constant 'type)
(putprop 'imply 'constant 'type)
(putprop 'equiv 'constant 'type)
(setq operators '(or and imply equiv)) ; Can't begin a literal
(setq mode 'assert)
(setq in-line 0)
(princ "Type HELP for help.\n\n")
)
;
;-------------------------------------------------------------------
;
; CLAUSE CONVERSION CODE
;
; Convert the fact to clause form
;
(defun clause-convert (fact)
(let
(
(result fact)
)
(cond
((atom fact) fact)
((literal-p fact) fact)
(t
(setq result (cc-equiv result))
(setq result (cc-imply result))
(setq result (cc-push-not result))
(setq result (cc-push-or result))
(setq result (cc-disassoc result))
result
)
)
)
)
;-------------------------------------------------------------------
;
; Convert clause form (equiv (a) (b)) -->
; (and (imply (a) (b)) (imply (b) (a)))
;
;
(defun cc-equiv (c)
(cond
((atom c) c)
((literal-p c) c)
((equal (car c) 'equiv)
`(and
(imply ,(cc-equiv (cadr c)) ,(cc-equiv (caddr c)))
(imply ,(cc-equiv (caddr c)) ,(cc-equiv (cadr c)))
)
)
(t (mapcar 'cc-equiv c))
)
)
;-------------------------------------------------------------------
;
; Convert clause form (imply (a) (b)) -->
; (or (not (a)) (b))
;
;
(defun cc-imply (c)
(cond
((atom c) c)
((literal-p c) c)
((equal (car c) 'imply)
`(or
(not ,(cc-imply (cadr c)))
,(cc-imply (caddr c))
)
)
(t (mapcar 'cc-imply c))
)
)
;-------------------------------------------------------------------
;
; Push NOTs down to literals -
; (not (not (a))) --> (a)
; (not (or (a) (b) (c))) --> (and (not (a)) (not (b)) (not (c)))
; (not (and (a) (b) (c))) --> (or (not (a)) (not (b)) (not (c)))
; (not (exist x (...)) --> (all x (not (...)))
; (not (all x (...)) --> (exist x (not (...)))
;
;
(defun cc-push-not (c) ; No prior NOT being pushed
(cond
((atom c) c)
((literal-p c) c)
((equal (car c) 'not) (cc-push-not* (cadr c)))
(t (mapcar 'cc-push-not c))
)
)
(defun cc-push-not* (c) ; Prior NOT being pushed
(cond
((atom c) c)
((literal-p c) (lit-negative c))
((equal (car c) 'not) (cc-push-not (cadr c)))
((equal (car c) 'and)
(append '(or) (mapcar 'cc-push-not* (cdr c)))
)
((equal (car c) 'or)
(append '(and) (mapcar 'cc-push-not* (cdr c)))
)
((equal (car c) 'exist)
(append `(all ,(cadr c)) (mapcar 'cc-push-not* (caddr c)))
)
((equal (car c) 'all)
(append `(exist ,(cadr c)) (mapcar 'cc-push-not* (caddr c)))
)
)
)
;----------------------------------------------------------------------
;
; Move all the ORs down below the AND's
;
;
(defun cc-push-or (c)
(cond
((atom c) c)
((literal-p c) c)
((equal (length c) 2) (cadr c)) ; (AND/OR (a)) --> (a)
((equal (car c) 'or)
(cc-or-merge
(cc-push-or (cadr c))
(cc-push-or (append '(or) (cddr c)))
)
)
(t (mapcar 'cc-push-or c))
)
)
;----------------------------------------------------------------------
;
; Merge two cleaned-up forms with an OR
;
;
(defun cc-or-merge (x y)
(cond
((null x) y)
((null y) (cc-or-merge y x))
((atom x)
(princ "Error in cc-or-merge - invalid form ")
(print x)
)
((atom y) (cc-or-merge y x))
((equal (car x) 'and)
(append
'(and)
(mapcar '(lambda (a) (cc-or-merge y a)) (cdr x))
)
)
((equal (car y) 'and) (cc-or-merge y x))
(t `(or ,x ,y))
)
)
;----------------------------------------------------------------------
;
; Flatten the form by the association rule
;
;
(defun cc-disassoc (c)
(cond
((atom c) c)
((literal-p c) c)
; (AND/OR (a)) --> (a)
((equal (length c) 2) (cc-disassoc (cadr c)))
(t
(cc-merge-assoc
(car c)
(cc-disassoc (cadr c))
(cc-disassoc (caddr c))
)
)
)
)
;----------------------------------------------------------------------
;
; Merge two cleaned-up forms by association
;
;
(defun cc-merge-assoc (op x y)
(cond
((null x) y)
((null y) (cc-merge-assoc op y x))
((atom x)
(princ "Error in cc-merge-assoc - invalid form ")
(print x)
)
((atom y) (cc-merge-assoc op y x))
(t
(append
(list op)
(cond
((equal (car x) op) (cdr x))
(t (list x))
)
(cond
((equal (car y) op) (cdr y))
(t (list y))
)
)
)
((equal (car y) 'and) (cc-merge-assoc y x))
(t `(or ,x ,y))
)
)
(qa)